
\section{Overview of the Proposed Approach}
\label{sec:ProposedWork}

\begin{figure}[!htp]
\centering
\includegraphics[scale=0.65]{fig/EMS.pdf}
\caption{Overview of the Evolution Modeling Approach}
\label{fig:EMS}
\end{figure}
In this section, we present an overview of our proposed approach to support evolution modeling for AADL. Our proposed extensions integrate the security patterns with AADL. We provide a mapping between the elements of AADL and the security pattern to reduce the dependencies between newly added patterns and existing architecture specification modeled using AADL. This work is based on raising the level of abstraction from  It provides the flexibility of security implementation for implementation logics and development platforms.

To map the security patterns to AADL elements, we analyzed both the security patterns and the elements of AADL meta-model. We define mappings between the AADL elements and the security patterns. The approach uses the model-transformations to transform an AADL model without security concerns into a security enabled AADL model. Figure \ref{fig:EMS} depicts our approach for integrating security into AADL. According to figure \ref{fig:EMS}, a transformation is specified for each security concern and applied to an AADL model to enable the security. For each security pattern a separate transformation is required to be specified. 


In this work, we take one important security concern \textsf{Confidentiality} as a security objective. We demonstrate how the confidentiality can be integrated at the architecture level by integrating different patterns related to confidentiality; such as  \textsf{Authentication Enforcer} and \textsf{Authorization Enforcer}. 

The next step of this work is to calculate satisfiability function considering the DREF delimitation of satisfiability function. In this work the DREF entity is the system under consideration. We are considering Barbados Crisis Management System as explained in the next section. We are applying satisfiability on different versions of this system, for instance one version without any security patterns, and another version with security property. 
We are using a Boolean satisfaction function with two values, a zero indicating that property is not satisfied by the entity and a 1 to indicate that property is satisfied by the entity. This helps us to evaluate the resilience of the system using DREF Framework. 

\marginpar{here you should guide the reader what should be in the next sub sections}

\section{Applying Proposed Work on Barbados Crash Management System Casestudy}
\label{CS}
In this section, we explain our approach with the help of Barbados Crash Management System Productline (bCMS) casestudy [Capozucca et al., 2011] \ref{}. The bCMS is a distributed crisis management system, which consists of two interacting sub systems; a Fire Station Coordinator System (FSCoordinator) and a Police Station Coordinator System(PSCS).  When a crises is notified to the both systems, an agreement of route selection should be achieved. For the FSCoordinator to deploy the fire trucks, the PSCS should send the route information. The scenario for this route coordination is presented below. 

\begin{enumerate}
\item{The PSCoordinator sends the event sendPSCrisisDetail to the PSCS system along with the crisis information. The PSCS system passes the crisis detail to FSCoordinator through FSCS system.}
\item{The FSCoordinator generates an even to reply firetrucks. Which is passed to PSCoordinator through PSCS and FSCS system.}
\item{The PSCoordinator proposes a firetrucks route. The route proposal is passed to PSCS, from there to FSCS and to the FSCoordinator.}
\end{enumerate}
\begin{figure}[!]
\includegraphics[width=\columnwidth]{fig/BBCMS1.png}%
\vspace{-0.2cm}
\caption{Barbadose Crisis Management System}.}%
\label{fig:BCMS1}%
\end{figure}

Figure \ref{fig:BCMS1}, presents the architecture of the system using AADL. The scenario presented above shows the communication between several system components. However, the confidentiality requirements are not addressed by the above presented scenario. To prevent unauthorized access, the system should support authentication and authorization properties. However, the initial version of the system lacks both authentication and authorization properties. In the next subsections, we discuss the \textsf{Authentication Enforcer} security pattern for enforcing confidentiality and our approach to integrate this pattern with AADL. 
%\begin{table}[!htp]
%\renewcommand{\arraystretch}{1.3}
%	\centering
%	\begin{scriptsize}
%		\begin{tabular}[htp!]{|c|c|c|}
%		\hline
%		\textbf{bCMS} & \textbf{Property} & \textbf{Satisfaction} \\
%		\hline
%		\hline
%		bCMS  & SP1= Authentication 
%		        SP2= Authorization   &   0\\
%		\hline
%	\end{tabular}
%	\end{scriptsize}
%	\caption{Mapping from Saf-Archie to SD} 
%	\label{table:mapc}
%\end{table}

\subsection {The Authentication Enforcer Pattern}
\marginpar{any reason why you have chosen this pattern}
As suggested by the name, the \textsf{Authentication Enforcer Pattern} \ref{} enforces an important security property \textsf{Authentication}[Steel 2005] in a given system \ref{}. Authentication might be required by several components of a given system. To introduce the authentication at the architectural level, in our approach, we use \textsf{Authentication Enforcer Pattern} \ref{}. As discussed earlier, introducing the authentication property at the architectural level enables the flexibility for the selection of different implementation strategies and platforms. Some example implementation strategies can be password based authentication \ref{}, client certificate based authentication \ref{} or Kerberos's \ref{} method of authentication. 
\begin{figure}[!htp]
\centering
\includegraphics[scale=0.65]{fig/AEP.png}%
\vspace{-0.2cm}
\caption{Authentication Enforcer Pattern}.}%
\label{fig:AEP}%
\end{figure}
\marginpar{figure reference????}

Figure \ref{fig:AEP} presents the \textsf{Authentication Enforcer Pattern},  which is one of the confidentiality patterns. 
The authentication enforcer pattern consists of four classes; a \textsf{Client} class, the \textsf{Authentication Enforcer}, the \textsf{Request Context}, and the \textsf{Subject} class. The client sends its credentials to the \textsf{Request Context} class. The \textsf{Authentication Enforcer} class takes the client credentials from the \textsf{Request Context} class. The \textsf{Authentication Enforcer} can implement the authentication mechanism and authenticates a \textsf{Request} from the \textsf{Client}. It then creates an instance of the \textsf{Subject} class, which represents an authenticated user. The \textsf{Client} then uses this subject instance to access different components of the application. 

\subsection {Applying Authentication Enforcer Pattern onto AADL: Using Model Transformations}
In this section, we present our mechanism for applying the \textsf{Authentication Enforcer Pattern} on AADL by using model transformations. We developed the mapping rules to embed the pattern inside an AADL specification.

\begin{table}[!htp]
\renewcommand{\arraystretch}{1.3}
	\centering
	\begin{scriptsize}
		\begin{tabular}[htp!]{|p{2cm}|p{4cm}|p{1.5cm}|p{2cm}|}
		\hline
		\textbf{Security Pattern Class} & \textbf{AADL class} & \textbf{Operation}& \textbf{Feature} \\
		\hline
		\hline
		  & System Component  & create  & In/out EventData Port  \\
		\hline
		Authentication Enforcer& Process Sub Component & create & In/out DataPort
		\\
		\hline
    Request Context & Data Sub Component of Process Component & create & \\
		\hline
		Subject & Data Sub Component of Process Component& & \\
		\hline
		
	\end{tabular}
	\end{scriptsize}
	\caption{Mapping Authentication Enforcer Pattern onto AADL } 
	\label{table:mapc}
\end{table}
\ref{where is the mapping for Client, why is it missing}

Table \ref{table:mapc} represents the mappings between the elements of AADL and the \textsf{Authentication Enforcer Pattern}. According to table \ref{table:mapc}, to apply the pattern, first an AADL \textsf{System Component} is required to be created. This component will contain all other sub component required to embed the \textsf{Authentication Enforcer Pattern}. The \textsf{Authentication Enforcer} class maps to a \textsf{Process Sub Component} in AADL. The reason for mapping a \textsf{Authentication Enforcer} to a \textsf{Process Sub Component} is that a \textsf{Authentication Enforcer} must contain the implementation logic. This implementation logic can be defined as thread of implementation inside a \textsf{Process Sub Component}. 

The \textsf{Subject} class and the \textsf{RequestContext} class are mapped to the \textsf{Data Sub Component} in AADL \marginpar{why give reasons for that}. 


The last operation executed will be a link operation that will link the whole system component for authentication enforcer to the client component.
\marginpar{this link part is not shown in the table, what are the Features column in the table. You have not discussed them in the text. }


\subsection {Applying Authentication Enforcer Pattern to bCMS using AADL}
\begin{figure}[!]
\includegraphics[width=\columnwidth]{fig/AEPAADL.png}%
\vspace{-0.2cm}
\caption{Authentication Enforcer Pattern and bCMS}.}%
\label{fig:AEPAADL}%
\end{figure}

We now apply the mappings defined in Table \ref{table:mapc} on the bCMS system as depicted in Figure{fig:AEPAADL}.To apply the mappings, we have performed the following steps: 
\begin{enemerate}
\item{Create a new System component called 'Authentication Enforcer' for each sub system in the bCMS System. We create two system components, one for PSCS System and the other for FSCS System. Each Authentication Enforcer System component has an in EventData port and an out EventData port to communicate with the respective client.}
\item{Inside the Authentication Enforcer System component, create a process sub-component named Authentication Enforcer that represents the class Authentication Enforcer in the security pattern class diagram. The process component is an abstraction to represent the actual logic of the authentication process.
}
\item{In the process sub-component implementation create two data components, one is for RequestContext class and the other for Subject class. The process implementation takes the data compoenent RequestContext as input from the client as it contains the client credentials, and generates data subcomponent Subject as output to the client. }
\item{
Link the new component Authentication Enforcer with the client component.}
\end{enumerate}

\marginpar{why suddenly bCMS turned to bCMS-1????}\subsection{Calculating Satisfaction Function for bCMS-1}

The satisfaction function for bCMS-1 is shown in Table 4. The entity bCMS-1 satisfies authentication property and hence value 1 and it does not satisfy authorization property and hence value is 0.

\begin{table}[!htp]
\renewcommand{\arraystretch}{1.3}
	\centering
	\begin{scriptsize}
		\begin{tabular}[htp!]{|c|c|c|}
		\hline
		\textbf{Entity} & \textbf{Property} & \textbf{Satisfaction} \\
		\hline
		\hline
		  bCMS1  & SP1=Authentication & 1  \\
		\hline
	bCMS1 & SP2=Authorization & 0
		\\
		\hline
		
	\end{tabular}
	\end{scriptsize}
	\caption{Confidentiality Properties of Different versions of bCMS} 
	\label{table:mapA1}
\end{table}

However, considering the authentication enforcer pattern only is not enough to ensure the confidentiality.
If a user is authenticated it never means he is authorized for every type of business functionality in the component. At minimum an application has two type of users a common user and an administrator. The access rights for a common user and an administrator are always different. In bCMS if a common user is using the system, he is just permitted to access the crisis information. 

1.	Suppose user U1 gets authenticated from the authentication enforcer component and gets the subject S1.
2.	U1 uses S1 to access the system. U1 is not authorized to view, read or right the crisis details within the system. 
3.	U1 uses the crisis details for which he is not authorized. 
The scenario shows that the system should define the access rights for all different users of the system to ensure confidentiality of the data. The follow subsection integrates authorization as a concern inside AADL by using the model transformation approach. 
\subsection {	Integrating Authorization Enforcer to AADL}

As discussed earlier, \texts{Authorization} is the property of the system which enables the verification of requests from users with respect to their allowed operations on system resources \ref{}[Steel et al  2005]. To improve security of the system, it is required that each request should not only be authenticated but authorized as well. A confidential application should ensure that the user access only that information that he is authorized to access. To provide authorization property in bCMS system we are using Authorization Enforcer pattern, originally proposed by Steel et al. \ref{} as shown in Figure \ref{fig:AuthE}.

\begin{figure}[!]
\includegraphics[width=\columnwidth]{fig/AuthE.png}%
\vspace{-0.2cm}
\caption{Authorization Enforcer Pattern}.}%
\label{fig:AuthE}%
\end{figure}

According to the Figure \ref{fig:AuthE}, The authorization enforcer pattern works with authentication enforcer to get verification details of the user. The SecureBasedAction class in authorization enforcer pattern interacts with request context to get the user credentials. It sends a request to the AuthorizationEnforcer class to authorize the subject. The AuthorizationEnforcer class in turns uses the AuthorizationProvider class that actually implements the authorization logic. The authorization Provider class creates the Permissions for the Subject.  The subject created possesses a set of permissions that define the authorizations of the subject. 

\subsection {Applying Authorization Enforcer Pattern to AADL: Using Model Transformations}

The authorization enforcer pattern can be applied to any AADL model using the model-transformation approach. Different authorization patterns can be used depending on the need; such as \textsf{Role Back Access Control} \ref{}, or \textsf{Session Pattern} \ref{}. Table \ref{table:MapA2} presents the rules to map authorization enforcer pattern to AADL meta-model. 

For each Authorization Enforcer component, create a new System component of AADL. This System component has many sub-components that support the complete pattern of authorization enforcer. We are creating two system sub-components SecureBasedAction and Authorization Enforcer system sub-component. The two components delegate the request of authorization to Authorization provide component. In this mapping Authorization Provider is a process sub-component that contains a thread for implementation logic. A permission data component is created that contains a sub program calculate permissions. The last operation is to link the Authorization Enforcer  component to Authentication Enforcer and the Client Component. 

\begin{table}[!htp]
\renewcommand{\arraystretch}{1.3}
	\centering
	\begin{scriptsize}
		\begin{tabular}[htp!]{|p{3cm}|p{3cm}|p{2cm}|p{2cm}|}
		\hline
		\textbf{Security Pattern Class} & \textbf{AADL class} & \textbf{Operation}& \textbf{Feature} \\
		\hline
		\hline
		  & Authorization Enforcer System Component  & create  & In/out EventData Port  \\
		\hline
		SecureBasedAction class& SecureBasedAction system sub-component & create & In/out EventdataPort
		\\
		\hline
    Authorization Enforcer Class & Authorization Enforcer system sub-component & create & In/out EventdataPort\\
		\hline
		AuthorizationProvider class & Process sub-component&            create& \\
		\hline
	& Thread sub-component in Process sub-component&            create& \\
		\hline
		Permission & Data sub-component Permission&        & \\
		\hline
		& Subprogram in Data sub-component Permission&            & \\
		\hline
	\end{tabular}
	\end{scriptsize}
	\caption{Mapping Authentication Enforcer to AADL} 
	\label{table:MapA2}
\end{table}

\subsection {Integrating Authorization Enforcer to AADL}

To integrate the authorization enforcer pattern with AADL we take following steps.
Create a system component Authorization Enforcer with the system. The component contain two ports, one in data event port to get subject information from AuthenticationProvider and one out Eventdata port to provide subject with set of permissions to client .
Create a SecureBasedAction sub-component with two ports, one out EventData port and another out EventdataPort. Create a subcomponent Authorization Enforcer with two Eventdataports, one in and one out port. Create a process subcomponent  called Authorization Provider. This component contains the actual logic to implement authorization component.
The implementation of  Process component contains at least one thread ( the number of threads can be more depending on the execution logic for authorization ), and a data subcomponent for data  store of permissions. The data component permission contains a server sub program which a method to calculate the permissions that are applicable for the given subject.
Connect the Authorization Enforcer with the Authentication Enforcer pattern. To get subject and with client component to provide subject.
We apply the above mappings on our bCMS example and create another version of bCMS with an improved security level. The integration is presented in fig 7.


\begin{figure}[!]
\includegraphics[width=\columnwidth]{fig/AuthoE.png}%
\vspace{-0.2cm}
\caption{Authorization Enforcer Pattern in bCMS}%
\label{fig:AuthoE}%
\end{figure}

The components Authorization EnforcerPS and Authorization EnforcerFS are implementation of an Authorization Enforcer System Component. The Authorization Enforcer PS is connected to Authentication Enforcer PS to get the authenticated subject and to client component for providing subject and a set of permission with the subject. Fig 8 is the internal representation of Authorization Enforcer Component. 

\begin{figure}[!]
\includegraphics[width=\columnwidth]{fig/Internal.png}%
\vspace{-0.2cm}
\caption{Internal Structure of Authorization Provider process sub Component
}%
\label{fig:AuthoE}%
\end{figure}

Fig 8 shows that Authorization Enforcer component contains Secure based action component, Authorization Enforcer component and Authorization Provider sun component. The figure gives a detail of the interconnections among components.

\begin{figure}[!]
\includegraphics[width=\columnwidth]{fig/Detail.png}%
\vspace{-0.2cm}
\caption{Internal Structure of AuthorizationProvider process sub Component
}%
\label{fig:AuthoE}%
\end{figure}

The authorization Provider sub-component contains a thread and a data component Permission as shown in fig.9. A code snipped of above implementation is shown in Table 6. 
Table 6. Authorization Enforcer Implementation

Add Listing....system implementation AuthorizationEnforcer.imp

Scenario of usage:

1.	ClientA sends client data to Authentication Enforcer subcomponent.
2.	The authentication enforcer authenticates the client and generates a subject.
3.	The subject instance is send to Authorization Enforcer subcomponent.
4.	The Authorization Enforcer authorizes the subject and attaches a set of permission.


Calculating Satisfaction Function for bCMS-2:

In Table 7 we calculate satisfaction of bCMS-2 as per DREF concepts.

\begin{table}[!htp]
\renewcommand{\arraystretch}{1.3}
	\centering
	\begin{scriptsize}
		\begin{tabular}[htp!]{|c|c|c|}
		\hline
		\textbf{Entity} & \textbf{Property} & \textbf{Satisfaction} \\
		\hline
		\hline
		  bCMS2  & SP1=Authentication & 1  \\
		\hline
	bCMS2 & SP2=Authorization & 1
		\\
		\hline
		

		
	\end{tabular}
	\end{scriptsize}
	\caption{Satifaction Function for bCMS-2} 
	\label{table:mapA1}
\end{table}

\subsection {Comparison of Satisfaction Level}


The comparison of satisfaction functions for different versions of bCMS is essential to calculate DREF resilience. In Table we see an overview of the comparison of satisfiability value for each property and also the global satisfiability function for different versions of bCMS. As it is event that gSAT for each version of the bCMS is increasing as compared to the previous version. We can see that degradation is reducing and satisfiability is increasing. As per DREF the system is said to be resilient with respect to the given properties. In fig 10 and fig 11 the comparison is plotted on the graph.


\begin{table}[!htp]
\renewcommand{\arraystretch}{1.3}
	\centering
	\begin{scriptsize}
		\begin{tabular}[htp!]{|c|c|c|}
		\hline
		\textbf{Entity} & \textbf{Property} & \textbf{Satisfaction} \\
		\hline
		\hline
		  bCMS & SP1=Authentication & 0  \\
		\hline
	bCMS & SP2=Authorization & 0
		\\
		\hline
				
		bCMS1 & SP1=Authentication & 1  \\
		\hline
	bCMS1 & SP2=Authorization & 0
		\\
		\hline
		bCMS2 & SP1=Authentication & 1  \\
		\hline
	bCMS2 & SP2=Authorization & 1
		\\
		\hline
		
	\end{tabular}
	\end{scriptsize}
	\caption{Comparison of the Satisfaction Functions} 
	\label{table:mapA}
\end{table}

ADD GRAPHS....

\section {Generating Protocol State machines from AADL Behavior Annex}
\marginpar{again it was mentioned no where in the proposed approach and you just are now talking about the protocol state machines, any motivations?? Any relation to the proposed approach section????}
\subsection {	Protocol State Machines}

UML Protocol state machines are of the state machines that capture the interface behavior of components. It is added in UML version 2. Protocol state machines are composed of states, transitions and guard conditions. Unlike the behavior state machines protocol state machines do not contains Actions, as they capture only the protocol of the interfaces. In fig 12 a simplified meta-model of pSM is shown. 

\begin{figure}[!]
\includegraphics[width=\columnwidth]{fig/pSMMM.png}%
\vspace{-0.2cm}
\caption{Protocol State Machine Meta-Model
}%
\label{fig:pSMMM}%
\end{figure}

\subsection {AADL Behavior Modeling}

The AADL behavior annex supports the representation of the behavior of AADL components. The AADL behavior annex has a number of features including
In AADL behavior annex the basic data types are defined in the package Basic types. The basic data types include integer, float, and Boolean. Data such as records can be shown using data hierarchies. In behavior annex we find some properties in property set that helps in defining complex data types such as arrays, for example the property 'Multiplicity' and 'multiplicities can be used to define one dimensional and multi dimensional arrays respectively. The property 'Abstract' can be used to define enumerations.  The behavior specifications can be attached to AADL specifications using an annex. The behavior annex is composed of following six sections.
Annex behavior-specification{**
<state variable>
<initializations>
<states>
<transitions>
<connections>
<composite_declarations>
**};

\begin{figure}[!]
\includegraphics[width=\columnwidth]{fig/AADLBA.png}%
\vspace{-0.2cm}
\caption{AADL Behavior Annex
}%
\label{fig:AADLBA}%
\end{figure}

4.3	ATM Example
We are using a simple ATM case study in our work. The ATM system has two components a client interface and an ATM system. Client is sending a request to authenticate user through an out Event Data port. ATM machine receives the request from client to authenticate along with the client credentials. We will use this simple case study to generate protocol state machines. 


\begin{figure}[!]
\includegraphics[width=\columnwidth]{fig/ATM.png}%
\vspace{-0.2cm}
\caption{AADL of ATM Example
}%
\label{fig:ATM}%
\end{figure}

4.4	Generating pSM from AADL Behavior Annex

The state variables are the type identifier of one of the AADL type. They must be initialized in the initialization section. The state section is used to declare states of the automaton. States can be initial, complete, return, urgent or composite states. Where initial state is the state where the state machine starts (execution), a return state ends a sub program. A complete state indicates completion of a thread. The states called urgent states are used in the context of model checking. The composite states represent a state with one or many region. The transition section defines system's transition from a source state to a target state. We can attach guards, Boolean conditions and actions with the transitions. AADL behavior annex can be used to show transition between different modes. A simple comparison of AADL behavior annex state and protocol state is shown in Table 9


\begin{table}[!htp]
\renewcommand{\arraystretch}{1.3}
	\centering
	\begin{scriptsize}
		\begin{tabular}[htp!]{|p{5cm}|p{5cm}|}
		\hline
		\textbf{AADL State} & \textbf{pSM State}  \\
		\hline
		\hline
		  Give the behavior of the component a classifier & Present an external view of a classifier  \\
		\hline
There is an initial state, some other states that show the behavior and then a final state & Initial and final states are compulsory for a pSM.
		\\
		\hline
		
		No actions associated with states & States cannot have an entry, exit or do activity actions  \\
		\hline
	
	\end{tabular}
	\end{scriptsize}
	\caption{Mapping from AADL State to pSM state} 
	\label{table:mappSM}
\end{table}



\begin{table}[!htp]
\renewcommand{\arraystretch}{1.3}
	\centering
	\begin{scriptsize}
		\begin{tabular}[htp!]{|p{5cm}|p{5cm}|}
		\hline
		\textbf{AADL Transition} & \textbf{pSM Transition}  \\
		\hline
		\hline
		  Can have events, Boolean conditions, expressions. & Has a pre-condition(guard), on trigger, and a post condition  \\
		\hline
Can be associated with more event. & Is associated to zero or more operations
		\\
		\hline
		
	Option to give transitions a number, that sets the priority. & Protocol order  \\
		\hline
	Pre and post conditions in the form of on and when clause, but is optional & Post condition must be represented  \\
		\hline
		
		No such restriction in AADL transition & Several transition can refer to same operation  \\
		\hline
		
			Mode transition concept& Composite states  \\
		\hline
	\end{tabular}
	\end{scriptsize}
	\caption{Mapping from AADL Transition to pSM Transition} 
	\label{table:mappSM1}
\end{table}

From table 9 and 10 we can see that it is possible to use pSM states and transitions to represent AADL states and transitions. 

Generating Protocol State Machines from ADL Behavior Annex

\begin{figure}[!]
\centering
\includegraphics[width=70mm]{fig/ATMpsm.png}%
\vspace{-0.2cm}
\caption{pSM to ATM Example
}%
\label{fig:ATMpsm}%
\end{figure}


\section {Perspectives of the Work}

In this section, we discuss the work that needs to be done in the domain of evolution modeling and pSM generation from AADL.

5.1	Evolution Modeling in AADL 
In this work we have proposed an evolution modeling support that is MDE based. We have proposed a solution that uses model transformation to integrate security patterns with software architecture. 
We intend to explore more on authorization security properties. We will use access control policies and merge the policies at software architecture level. We intend to propose a meta-model that covers role based access control policy, model transformations for it and integration of access control policies with software architecture. At large we are working on a domain specific language to express access control policies and its integration with the software architecture. The automation of the work is an important part of our future work. The goal is to integrate the DSL with existing AADL took OSATE . The application of work on REACT Case Study is one of the important parts of our research.
5.2	pSM Generation from AADL Behavior Annex
So far we have analyzed the use of AADL behavior annex to generate pSM for each component of the software architecture. We are interested in testing the behavior of the system. To capture behavior of the whole system, we intend to compose protocol state machines for individual components. The composite state machines will provide a view of the behavior of the whole system.  The next step of this work is to generate behavior of the whole system and later use SESAME approach for test selection from these pSM. 
